.. SPDX-License-Identifier: GPL-2.0 or GPL-3.0
.. Copyright © 2019 Ariadne Devos

Verification problems to solve
==============================

As of now, s² is written in C (executable) annotated in ACSL
(logical), which is processed by Frama-C to produce logical
verification conditions (unverified) to submit to (typically
unverified, possibly in conflicting logics) automatic theorem
provers. It would be preferable to write everything in Coq, with
its small logical core.

Lack of expressivity
--------------------
Internet RFC often refer to syntax defined by regular expressions.
Regular expressions aren't hard to define in Coq by induction,
but ACSL inductive predicates can be inconsistent. SMT solvers
can't solve everything, do not respect modularity and sometimes
require many hints. Coq is just more general.

Queue of theories to formulate or integrate
------------------------------------------

(In order of rough priority)
(Preferably already done by someone else)

- a theory of applicative functors
  (for verified program generation)
- positional number systems (number -> digits)
  (for many RFCs)
- sequential memory model
- subset of C (expressions, control and effects)
- extracting the subset of C (to compile it)
  (or, later: feed it to a free, verified compiler)
- positional number systems (<sHT/math/positional.h>)

(Later)
- I/O models
- concurrent memory models?
- timing, information flow?

Formalised theores, maybe to document
-------------------------------------

- Arrow lifting, arrow laws
- Regular expresions (Language)
- Co-inductive lists (Trace)
- Lattices (Lattice)
- positional numbers (digits -> S.Numeric.Positional)
